These are archival webpages, generated on 2023-03-20 by Prove-It Beta Version 0.3, licensed under the GNU Public Licence by Sandia Corporation. See pyproveit.org for the lastest version.
logo
In [1]:
import proveit
theory = proveit.Theory() # the theorem's theory
from proveit import a, b, c, k, m, n, t, P, defaults, Function
from proveit.linear_algebra import ScalarMult, TensorProd, VecSpaces
from proveit.logic import Equals, InSet
from proveit.numbers import (
        zero, one, two, i, e, pi, Add, Sum, Exp, Less, LessEq, Mult, frac, Neg, subtract)
from proveit.numbers import Complex, Interval, Natural
from proveit.numbers.number_sets.natural_numbers import fold_forall_natural_pos
from proveit.physics.quantum import Ket, NumKet
from proveit.physics.quantum.QPE import _phase, _phase_is_real, _psi_t_def
In [2]:
%proving _psi_t_formula
Under these presumptions, we begin our proof of
_psi_t_formula:
(see dependencies)

Keep the $2$ in $2 \pi i$ from combining with powers of $2$:

In [3]:
Exp.change_simplification_directives(factor_numeric_rational=True)
In [4]:
# the induction theorem for positive naturals
fold_forall_natural_pos
In [5]:
# instantiate the induction theorem
induction_inst = fold_forall_natural_pos.instantiate(
    {Function(P,t):_psi_t_formula.instance_expr, m:t, n:t})
induction_inst:  ⊢  

Base Case

In [6]:
VecSpaces.default_field=Complex
defaults.assumptions = _psi_t_formula.all_conditions()
defaults.assumptions:
In [7]:
base_case = induction_inst.antecedent.operands[0]
base_case:

We have $|\psi_{t}\rangle$ defined as a tensor product (the result of the first phase of the quantum circuit, and the LHS of Nielsen & Chuang's identity 5.20 on pg 222):

In [8]:
_psi_t_def
In [9]:
_psi_t_as_tensor_prod = _psi_t_def.instantiate()
_psi_t_as_tensor_prod:  ⊢  

For $\psi'_{1}$, we prove a useful equality then instantiate the psi_t_def with $t=1$:

In [10]:
psi_1_def = _psi_t_def.instantiate({t:one})
psi_1_def:  ⊢  

Then show that the summation formula also gives the same qbit result

In [11]:
sum_0_to_1 = base_case.rhs
sum_0_to_1:
In [12]:
sum_0_to_1_processed_01 = sum_0_to_1.inner_expr().operands[1].partitioning_first()
sum_0_to_1_processed_01:  ⊢  
In [13]:
# finish off the Base Case
base_case_jdgmt = sum_0_to_1_processed_01.sub_left_side_into(psi_1_def)
base_case_jdgmt:  ⊢  

Inductive Step

In [14]:
inductive_step = induction_inst.antecedent.operands[1]
inductive_step:
In [15]:
defaults.assumptions = defaults.assumptions + inductive_step.conditions.entries
defaults.assumptions:

First, partition the summation: $\sum_{k=0}^{2^{t+1}-1} e^{2\pi i \varphi k} |k\rangle_{t+1} = \sum_{k=0}^{2^{t}-1} e^{2\pi i \varphi k} |k\rangle_{t+1} + \sum_{k=2^{t}}^{2^{t+1}-1} e^{2\pi i \varphi k} |k\rangle_{t+1}$

In [16]:
desired_domain = _psi_t_formula.instance_expr.rhs.scaled.domain
desired_domain:
In [17]:
summation_partition_01 = (
    inductive_step.instance_expr.rhs.operands[1]
    .partitioning(desired_domain.upper_bound))
summation_partition_01:  ⊢  

Then shift the second summation of that partition, so that the two summations then have the same index domain:

In [18]:
summation_partition_02 = (summation_partition_01.inner_expr().rhs.
                          operands[1].shift(Neg(Exp(two, t))))
summation_partition_02:  ⊢  

We want to rewrite the summand of that 2nd summation on the rhs now by (1) expanding the exponential term and (2) rewriting the $|k+2^t{\rangle}_{t+1}$ ket as $|1\rangle \otimes |k{\rangle}_t$. This takes a little work.

In [19]:
rhs_2nd_sum = summation_partition_02.rhs.operands[1]
rhs_2nd_sum:
In [20]:
summand_processed_01 = rhs_2nd_sum.summand.inner_expr().operands[0].exponent.distribution(
    4, assumptions=[*defaults.assumptions,
                    rhs_2nd_sum.condition])
summand_processed_01: ,  ⊢  
In [21]:
summand_processed_02 = (
    summand_processed_01.inner_expr().rhs.operands[0]
    .exponent_separate(
        assumptions=[*defaults.assumptions,
                     InSet(k, Interval(zero, subtract(Exp(two, t), one)))]))
summand_processed_02: ,  ⊢  
In [22]:
# Avoid recombining these via auto-simplification
defaults.preserved_exprs = set([summand_processed_02.rhs.scalar])
defaults.preserved_exprs:
In [23]:
from proveit.physics.quantum.algebra import prepend_num_ket_with_one_ket
prepend_num_ket_with_one_ket
In [24]:
prepend_num_ket_with_one_ket_inst = prepend_num_ket_with_one_ket.instantiate(
        {n: t, k: k},
        assumptions=[*defaults.assumptions, InSet(k, Interval(zero, subtract(Exp(two, t), one)))])
prepend_num_ket_with_one_ket_inst: ,  ⊢  
In [25]:
summand_processed_03 = (
    summand_processed_02.inner_expr().rhs.operands[1]
    .substitute(prepend_num_ket_with_one_ket_inst))
summand_processed_03: ,  ⊢  
In [26]:
# reminder of summation_partition_03
summation_partition_02
In [27]:
summation_partition_04 = (
    summation_partition_02.inner_expr().rhs.operands[1].summand.substitute(
        summand_processed_03))
summation_partition_04:  ⊢  

Also process the summand in the 1st sum on the rhs, converting the ket $|k\rangle_{t+1}$ to the tensor product $|0\rangle \otimes |k\rangle_{t}$:

In [28]:
# pull up the relevant NumKet theorem
from proveit.physics.quantum.algebra import prepend_num_ket_with_zero_ket
prepend_num_ket_with_zero_ket
In [29]:
# instantiate the theorem for our specific case
prepend_num_ket_with_zero_ket_inst = prepend_num_ket_with_zero_ket.instantiate(
        {n: t, k: k},
        assumptions=[*defaults.assumptions, InSet(k, Interval(zero, subtract(Exp(two, t), one)))])
prepend_num_ket_with_zero_ket_inst: ,  ⊢  
In [30]:
# use our instantiation to substitute
summation_partition_05 = (
    summation_partition_04.inner_expr().rhs.operands[0].summand.scaled.substitute(
    prepend_num_ket_with_zero_ket_inst))
summation_partition_05:  ⊢  
In [31]:
coef = inductive_step.instance_expr.rhs.scalar
summation_partition_06 = summation_partition_05.scalar_mult_both_sides(coef)
summation_partition_06:  ⊢  
In [32]:
# Recall our inductive hypothesis:
inductive_hypothesis = defaults.assumptions[-1]
inductive_hypothesis:
In [33]:
conclusion_01 = summation_partition_06.inner_expr().rhs.factor(
        inductive_hypothesis.rhs, pull='right', field=Complex)
conclusion_01:  ⊢  
In [34]:
# use the inductive hypothesis:
conclusion_02 = inductive_hypothesis.sub_left_side_into(conclusion_01)
conclusion_02: ,  ⊢  

The RHS of conclusion02 above should be equal to $|\psi{t+1}\rangle$. Let's see how to get there. Ideally we could use the next three cells to show the rhs of the equality in `conclusion_02` is equal to $|\psi_{t+1}\rangle$

In [35]:
# reminder
_psi_t_def
In [36]:
psi_t_plus_one_as_tensor_prod = _psi_t_def.instantiate({t:Add(t, one)})
psi_t_plus_one_as_tensor_prod:  ⊢  

Now this substitute() step will also manage to pull the scalar coefficients out to the front in the process:

In [37]:
conclusion_03 = conclusion_02.inner_expr().rhs.operands[1].substitute(
        _psi_t_as_tensor_prod)
conclusion_03: ,  ⊢  

Now we partition the tensor product expression of $\psi_{t+1}$, so we can eventually show that it is equal to the rhs of conclusion_03.

In [38]:
psi_t_plus_one_as_tensor_prod.rhs
In [39]:
# # we can partition the operands in the psi_{t+1} tensor prod expression
psi_t_plus_one_as_tensor_prod_02 = (
    psi_t_plus_one_as_tensor_prod.inner_expr().rhs.operands[0].split(t))
psi_t_plus_one_as_tensor_prod_02:  ⊢  
In [40]:
conclusion_03.inner_expr().rhs.substitute(psi_t_plus_one_as_tensor_prod_02.derive_reversed())
In [41]:
# # recall our earlier instantiation of the induction theorem:
induction_inst

We have proven both pieces of the antecedent (i.e., the base case and inductive case) of the instantiated induction theorem induction_inst, so we can now derive the consequent:

In [42]:
induction_inst.derive_consequent()
_psi_t_formula has been proven.  Now simply execute "%qed".
In [43]:
%qed
proveit.physics.quantum.QPE._psi_t_formula has been proven.
Out[43]:
 step typerequirementsstatement
0modus ponens1, 2  ⊢  
1instantiation3, 4*, 5*, 6*  ⊢  
  : , : , :
2instantiation7, 8, 9  ⊢  
  : , :
3conjecture  ⊢  
 proveit.numbers.number_sets.natural_numbers.fold_forall_natural_pos
4instantiation601, 10, 449  ⊢  
  : , : , :
5instantiation11, 12  ⊢  
  :
6instantiation601, 13, 14  ⊢  
  : , : , :
7theorem  ⊢  
 proveit.logic.booleans.conjunction.and_if_both
8instantiation427, 15, 16  ⊢  
  : , : , :
9generalization17  ⊢  
10instantiation615, 630  ⊢  
  : , : , :
11conjecture  ⊢  
 proveit.physics.quantum.algebra.single_qubit_num_ket
12instantiation18, 19, 20  ⊢  
  :
13instantiation615, 126  ⊢  
  : , : , :
14instantiation460, 21  ⊢  
  : , :
15instantiation102, 679, 22, 23*  ⊢  
  :
16instantiation615, 24  ⊢  
  : , : , :
17instantiation460, 25,  ⊢  
  : , :
18conjecture  ⊢  
 proveit.numbers.number_sets.integers.nonneg_int_is_natural
19instantiation682, 26, 28  ⊢  
  : , : , :
20instantiation27, 636, 663, 28  ⊢  
  : , : , :
21instantiation29, 644, 679, 671, 630*  ⊢  
  : , : , :
22instantiation543, 30, 31  ⊢  
  : , : , :
23instantiation601, 32, 33  ⊢  
  : , : , :
24instantiation34, 636, 663, 35, 36*, 37*  ⊢  
  : , : , : , :
25instantiation543, 38, 39,  ⊢  
  : , : , :
26instantiation635, 636, 663  ⊢  
  : , :
27conjecture  ⊢  
 proveit.numbers.number_sets.integers.interval_lower_bound
28assumption  ⊢  
29conjecture  ⊢  
 proveit.numbers.exponentiation.product_of_posnat_powers
30instantiation477, 344, 613, 299  ⊢  
  : , : , :
31instantiation492, 613, 575  ⊢  
  : , :
32instantiation615, 40  ⊢  
  : , : , :
33instantiation41, 485, 42  ⊢  
  : , : , :
34conjecture  ⊢  
 proveit.linear_algebra.addition.vec_sum_split_first
35conjecture  ⊢  
 proveit.numbers.numerals.decimals.less_0_1
36instantiation601, 43, 44  ⊢  
  : , : , :
37instantiation601, 45, 46  ⊢  
  : , : , :
38instantiation543, 47, 48, 49*,  ⊢  
  : , : , :
39instantiation601, 50, 51  ⊢  
  : , : , :
40instantiation52, 679, 53  ⊢  
  : , : , :
41axiom  ⊢  
 proveit.linear_algebra.tensors.unary_tensor_prod_def
42instantiation453, 485, 203, 54  ⊢  
  : , : , : , :
43instantiation615, 55  ⊢  
  : , : , :
44instantiation56, 613, 325, 485  ⊢  
  : , : , :
45instantiation615, 57  ⊢  
  : , : , :
46instantiation58, 663, 59*  ⊢  
  : , :
47instantiation427, 60, 61,  ⊢  
  : , : , :
48instantiation102, 671  ⊢  
  :
49instantiation601, 62, 63  ⊢  
  : , : , :
50instantiation460, 64  ⊢  
  : , :
51instantiation460, 65  ⊢  
  : , :
52conjecture  ⊢  
 proveit.core_expr_types.tuples.tuple_eq_via_elem_eq
53instantiation615, 66  ⊢  
  : , : , :
54instantiation324, 485, 325, 67  ⊢  
  : , : , : , :
55instantiation601, 68, 69  ⊢  
  : , : , :
56conjecture  ⊢  
 proveit.linear_algebra.scalar_multiplication.one_as_scalar_mult_id
57modus ponens70, 71  ⊢  
58axiom  ⊢  
 proveit.linear_algebra.addition.vec_sum_single
59instantiation591, 421, 610, 422, 612, 644, 567, 580, 581  ⊢  
  : , : , : , :
60instantiation543, 72, 73  ⊢  
  : , : , :
61assumption  ⊢  
62instantiation74, 672, 194, 610, 164, 106, 612, 485, 107, 108, 75, 110  ⊢  
  : , : , : , : , : , : , : , : , : , :
63instantiation456, 281, 610, 194, 612, 164, 106, 485, 107, 108, 278, 110  ⊢  
  : , : , : , : , : , : , : , : , : , :
64instantiation76, 684, 77, 78, 79, 80  ⊢  
  : , : , : , :
65instantiation81, 158, 82, 83, 84, 85, 86*  ⊢  
  : , : , : , :
66instantiation615, 87  ⊢  
  : , : , :
67instantiation453, 485, 88, 488  ⊢  
  : , : , : , :
68instantiation615, 89  ⊢  
  : , : , :
69instantiation302, 490  ⊢  
  :
70instantiation90, 679  ⊢  
  : , : , : , : , : , :
71generalization91  ⊢  
72instantiation92, 93  ⊢  
  : , : , :
73instantiation601, 94, 95  ⊢  
  : , : , :
74conjecture  ⊢  
 proveit.linear_algebra.tensors.tensor_prod_disassociation
75instantiation453, 485, 281, 278  ⊢  
  : , : , : , :
76axiom  ⊢  
 proveit.core_expr_types.operations.operands_substitution
77instantiation624  ⊢  
  : , :
78instantiation624  ⊢  
  : , :
79instantiation460, 437  ⊢  
  : , :
80instantiation615, 96  ⊢  
  : , : , :
81conjecture  ⊢  
 proveit.logic.equality.sub_in_right_operands_via_tuple
82instantiation283, 97, 98, 101  ⊢  
  : , : , : , :
83instantiation283, 99, 100, 101  ⊢  
  : , : , : , :
84instantiation102, 638, 103  ⊢  
  :
85instantiation104, 105, 292*  ⊢  
  : , : , :
86instantiation456, 203, 610, 194, 612, 164, 106, 485, 107, 108, 109, 110  ⊢  
  : , : , : , : , : , : , : , : , : , :
87instantiation615, 111  ⊢  
  : , : , :
88instantiation540, 490, 112  ⊢  
  : , :
89instantiation113, 421, 610, 422, 612, 644, 567, 580, 581  ⊢  
  : , : , : , :
90axiom  ⊢  
 proveit.core_expr_types.lambda_maps.lambda_substitution
91instantiation615, 114  ⊢  
  : , : , :
92theorem  ⊢  
 proveit.linear_algebra.scalar_multiplication.scalar_mult_eq
93instantiation142, 115, 116  ⊢  
  : , :
94instantiation615, 117  ⊢  
  : , : , :
95instantiation460, 118  ⊢  
  : , :
96instantiation460, 135  ⊢  
  : , :
97instantiation543, 119, 120  ⊢  
  : , : , :
98instantiation572  ⊢  
  :
99instantiation121, 681, 122, 123, 124, 125, 194, 157*, 164*  ⊢  
  : , : , : , :
100instantiation460, 126  ⊢  
  : , :
101instantiation460, 127  ⊢  
  : , :
102axiom  ⊢  
 proveit.physics.quantum.QPE._psi_t_def
103instantiation601, 128, 129  ⊢  
  : , : , :
104conjecture  ⊢  
 proveit.core_expr_types.tuples.partition_front
105instantiation130, 610, 191  ⊢  
  : , :
106instantiation283, 131, 410, 134  ⊢  
  : , : , : , :
107instantiation132, 620, 636, 485, 168  ⊢  
  : , : , :
108instantiation283, 133, 410, 134  ⊢  
  : , : , : , :
109instantiation543, 278, 135  ⊢  
  : , : , :
110modus ponens136, 137  ⊢  
111instantiation615, 138  ⊢  
  : , : , :
112instantiation543, 139, 140  ⊢  
  : , : , :
113conjecture  ⊢  
 proveit.numbers.multiplication.mult_zero_any
114instantiation615, 141  ⊢  
  : , : , :
115instantiation142, 143, 144  ⊢  
  : , :
116instantiation615, 145, 146*, 147*, 148*  ⊢  
  : , : , :
117instantiation601, 149, 150  ⊢  
  : , : , :
118instantiation283, 151, 152, 153  ⊢  
  : , : , : , :
119instantiation193, 154  ⊢  
  : , : , :
120instantiation601, 155, 156  ⊢  
  : , : , :
121conjecture  ⊢  
 proveit.core_expr_types.tuples.general_len
122instantiation624  ⊢  
  : , :
123instantiation624  ⊢  
  : , :
124instantiation624  ⊢  
  : , :
125instantiation427, 672, 157  ⊢  
  : , : , :
126instantiation492, 618, 613  ⊢  
  : , :
127instantiation197, 158  ⊢  
  : , :
128instantiation615, 159  ⊢  
  : , : , :
129instantiation601, 160, 161  ⊢  
  : , : , :
130conjecture  ⊢  
 proveit.numbers.addition.add_nat_closure_bin
131instantiation543, 162, 164  ⊢  
  : , : , :
132conjecture  ⊢  
 proveit.logic.booleans.conjunction.redundant_conjunction_general
133instantiation543, 163, 164  ⊢  
  : , : , :
134instantiation460, 165  ⊢  
  : , :
135instantiation615, 166  ⊢  
  : , : , :
136instantiation167, 620, 636, 168  ⊢  
  : , : , : , :
137generalization169  ⊢  
138instantiation601, 170, 171  ⊢  
  : , : , :
139instantiation579, 546, 564  ⊢  
  : , :
140instantiation601, 172, 173  ⊢  
  : , : , :
141instantiation615, 299  ⊢  
  : , : , :
142theorem  ⊢  
 proveit.logic.equality.rhs_via_equality
143instantiation543, 174, 175  ⊢  
  : , : , :
144instantiation615, 176, 177*, 178*, 179*  ⊢  
  : , : , :
145modus ponens180, 181  ⊢  
146instantiation318, 622  ⊢  
  : , :
147instantiation318, 622  ⊢  
  : , :
148instantiation460, 182  ⊢  
  : , :
149instantiation615, 183  ⊢  
  : , : , :
150modus ponens184, 185  ⊢  
151instantiation601, 186, 187, 188*  ⊢  
  : , : , :
152instantiation615, 189  ⊢  
  : , : , :
153instantiation572  ⊢  
  :
154instantiation235, 547, 190, 610, 191, 672  ⊢  
  : , :
155instantiation615, 292  ⊢  
  : , : , :
156instantiation345, 610, 684, 612, 611, 618, 613  ⊢  
  : , : , : , :
157instantiation341, 613, 310  ⊢  
  : , : , :
158instantiation682, 670, 638  ⊢  
  : , : , :
159instantiation291, 618, 613  ⊢  
  : , :
160instantiation552, 610, 684, 672, 612, 192, 408, 575, 613  ⊢  
  : , : , : , : , : , :
161instantiation309, 613, 408, 310  ⊢  
  : , : , :
162instantiation193, 194  ⊢  
  : , : , :
163instantiation193, 194  ⊢  
  : , : , :
164instantiation601, 195, 196  ⊢  
  : , : , :
165instantiation197, 661  ⊢  
  : , :
166instantiation615, 198  ⊢  
  : , : , :
167conjecture  ⊢  
 proveit.logic.booleans.conjunction.conjunction_from_quantification
168instantiation374, 199, 257, 631, 200, 201*, 202*  ⊢  
  : , : , :
169instantiation453, 485, 203, 204,  ⊢  
  : , : , : , :
170instantiation615, 205  ⊢  
  : , : , :
171instantiation591, 547, 672, 296, 644, 567, 580, 581  ⊢  
  : , : , : , :
172instantiation574, 672, 684, 610, 565, 612, 546, 580, 581  ⊢  
  : , : , : , : , : , :
173instantiation574, 610, 684, 612, 548, 565, 644, 567, 580, 581  ⊢  
  : , : , : , : , : , :
174instantiation206, 636, 637, 211, 207, 208, 209*  ⊢  
  : , : , : , : , :
175instantiation210, 649, 211, 446, 212*, 213*, 214*  ⊢  
  : , : , : , : , :
176modus ponens215, 216  ⊢  
177instantiation318, 622  ⊢  
  : , :
178instantiation318, 622  ⊢  
  : , :
179instantiation283, 217, 218, 219  ⊢  
  : , : , : , :
180instantiation359, 679  ⊢  
  : , : , : , : , : , : , :
181generalization220  ⊢  
182modus ponens221, 222  ⊢  
183instantiation460, 223  ⊢  
  : , :
184instantiation224, 610, 684, 672, 225, 612, 226  ⊢  
  : , : , : , : , : , : , : , :
185instantiation645, 227, 231  ⊢  
  : , : , :
186instantiation456, 281, 610, 672, 612, 485, 486, 278, 228  ⊢  
  : , : , : , : , : , : , : , : , : , :
187instantiation615, 229  ⊢  
  : , : , :
188instantiation230, 454, 231, 281, 282, 232*  ⊢  
  : , : , : , : , :
189instantiation460, 233  ⊢  
  : , :
190instantiation568  ⊢  
  : , : , :
191instantiation682, 670, 234  ⊢  
  : , : , :
192instantiation624  ⊢  
  : , :
193conjecture  ⊢  
 proveit.core_expr_types.tuples.range_len
194instantiation235, 547, 236, 610, 237, 672  ⊢  
  : , :
195instantiation615, 238  ⊢  
  : , : , :
196instantiation283, 239, 240, 241  ⊢  
  : , : , : , :
197conjecture  ⊢  
 proveit.core_expr_types.tuples.range_from1_len
198instantiation615, 242  ⊢  
  : , : , :
199instantiation682, 668, 243  ⊢  
  : , : , :
200instantiation244, 245  ⊢  
  : , :
201instantiation601, 246, 247  ⊢  
  : , : , :
202instantiation283, 248, 310, 249  ⊢  
  : , : , : , :
203instantiation458, 613, 465, 466  ⊢  
  : , :
204instantiation324, 485, 325, 250,  ⊢  
  : , : , : , :
205instantiation601, 251, 252  ⊢  
  : , : , :
206conjecture  ⊢  
 proveit.linear_algebra.addition.vec_sum_split_after
207instantiation253, 254  ⊢  
  : , :
208instantiation255, 256, 257, 542, 258, 259*, 260*  ⊢  
  : , : , :
209instantiation601, 261, 262  ⊢  
  : , : , :
210conjecture  ⊢  
 proveit.linear_algebra.addition.vec_sum_index_shift
211instantiation648, 445, 650  ⊢  
  : , :
212instantiation409, 525, 263  ⊢  
  : , :
213instantiation601, 264, 265  ⊢  
  : , : , :
214instantiation339, 525  ⊢  
  :
215instantiation359, 679  ⊢  
  : , : , : , : , : , : , :
216generalization266  ⊢  
217instantiation615, 267, 268*, 269*  ⊢  
  : , : , :
218instantiation460, 270  ⊢  
  : , :
219instantiation615, 271  ⊢  
  : , : , :
220instantiation272, 671, 622,  ⊢  
  : , :
221instantiation392, 672, 679, 610, 454, 612  ⊢  
  : , : , : , : , : , : , : , : , : , : , :
222generalization273  ⊢  
223instantiation456, 390, 610, 672, 612, 485, 486, 488, 279  ⊢  
  : , : , : , : , : , : , : , : , : , :
224conjecture  ⊢  
 proveit.linear_algebra.tensors.tensor_prod_factorization_from_add
225instantiation509, 274  ⊢  
  :
226instantiation624  ⊢  
  : , :
227instantiation275, 681, 276, 510  ⊢  
  : , : , :
228instantiation453, 486, 282, 279  ⊢  
  : , : , : , :
229instantiation456, 282, 672, 610, 612, 485, 486, 278, 279  ⊢  
  : , : , : , : , : , : , : , : , : , :
230conjecture  ⊢  
 proveit.linear_algebra.scalar_multiplication.doubly_scaled_as_singly_scaled
231instantiation483, 681, 484, 485, 486, 277, 278, 279  ⊢  
  : , : , : , :
232instantiation280, 281, 282  ⊢  
  : , :
233instantiation283, 284, 285, 286  ⊢  
  : , : , : , :
234instantiation287, 288  ⊢  
  :
235conjecture  ⊢  
 proveit.numbers.addition.add_nat_closure
236instantiation568  ⊢  
  : , : , :
237instantiation289, 290  ⊢  
  :
238instantiation291, 408, 613, 292*  ⊢  
  : , :
239instantiation552, 672, 684, 293, 344, 618, 575, 613  ⊢  
  : , : , : , : , : , :
240instantiation345, 610, 547, 612, 294, 618, 575, 613  ⊢  
  : , : , : , :
241instantiation309, 613, 618, 310  ⊢  
  : , : , :
242instantiation295, 547, 672, 610, 296, 612, 644, 567, 580, 581, 525  ⊢  
  : , : , : , : , : , : , :
243instantiation682, 677, 620  ⊢  
  : , : , :
244conjecture  ⊢  
 proveit.numbers.ordering.relax_less
245instantiation304, 671  ⊢  
  :
246instantiation552, 672, 684, 610, 340, 612, 344, 408, 613  ⊢  
  : , : , : , : , : , :
247instantiation345, 610, 684, 612, 340, 408, 613  ⊢  
  : , : , : , :
248instantiation601, 297, 298  ⊢  
  : , : , :
249instantiation460, 299  ⊢  
  : , :
250instantiation453, 485, 300, 488,  ⊢  
  : , : , : , :
251instantiation615, 301  ⊢  
  : , : , :
252instantiation302, 644  ⊢  
  :
253conjecture  ⊢  
 proveit.numbers.addition.subtraction.nonneg_difference
254instantiation407, 510  ⊢  
  :
255conjecture  ⊢  
 proveit.numbers.addition.strong_bound_via_left_term_bound
256instantiation682, 668, 303  ⊢  
  : , : , :
257conjecture  ⊢  
 proveit.numbers.number_sets.real_numbers.zero_is_real
258instantiation304, 510  ⊢  
  :
259instantiation601, 305, 306  ⊢  
  : , : , :
260instantiation601, 307, 308  ⊢  
  : , : , :
261instantiation552, 610, 684, 672, 612, 346, 525, 575, 613  ⊢  
  : , : , : , : , : , :
262instantiation309, 613, 525, 310  ⊢  
  : , : , :
263instantiation572  ⊢  
  :
264instantiation552, 610, 684, 672, 612, 311, 352, 575, 353  ⊢  
  : , : , : , : , : , :
265instantiation601, 312, 313  ⊢  
  : , : , :
266instantiation543, 314, 315,  ⊢  
  : , : , :
267modus ponens316, 317  ⊢  
268instantiation318, 622  ⊢  
  : , :
269instantiation318, 622  ⊢  
  : , :
270modus ponens319, 320  ⊢  
271instantiation460, 321  ⊢  
  : , :
272conjecture  ⊢  
 proveit.physics.quantum.algebra.prepend_num_ket_with_zero_ket
273instantiation483, 681, 484, 485, 486, 322, 325, 366,  ⊢  
  : , : , : , :
274instantiation323, 681, 510  ⊢  
  : , :
275conjecture  ⊢  
 proveit.linear_algebra.tensors.tensor_prod_of_cart_exps_within_cart_exp
276instantiation624  ⊢  
  : , :
277instantiation624  ⊢  
  : , :
278instantiation324, 485, 325, 326  ⊢  
  : , : , : , :
279modus ponens327, 328  ⊢  
280axiom  ⊢  
 proveit.linear_algebra.scalar_multiplication.scalar_mult_extends_number_mult
281instantiation458, 613, 329, 330  ⊢  
  : , :
282instantiation458, 613, 331, 332  ⊢  
  : , :
283conjecture  ⊢  
 proveit.logic.equality.four_chain_transitivity
284instantiation601, 333, 334  ⊢  
  : , : , :
285instantiation572  ⊢  
  :
286instantiation460, 335  ⊢  
  : , :
287conjecture  ⊢  
 proveit.numbers.negation.nat_pos_closure
288instantiation336, 671  ⊢  
  :
289conjecture  ⊢  
 proveit.numbers.negation.nat_closure
290instantiation337, 620, 338  ⊢  
  :
291conjecture  ⊢  
 proveit.numbers.negation.distribute_neg_through_binary_sum
292instantiation339, 618  ⊢  
  :
293instantiation624  ⊢  
  : , :
294instantiation568  ⊢  
  : , : , :
295conjecture  ⊢  
 proveit.numbers.multiplication.leftward_commutation
296instantiation568  ⊢  
  : , : , :
297instantiation552, 672, 684, 610, 340, 612, 618, 408, 613  ⊢  
  : , : , : , : , : , :
298instantiation341, 618, 613, 410  ⊢  
  : , : , :
299instantiation342, 613  ⊢  
  :
300instantiation540, 490, 343,  ⊢  
  : , :
301conjecture  ⊢  
 proveit.numbers.negation.negated_zero
302conjecture  ⊢  
 proveit.numbers.exponentiation.exp_zero_eq_one
303instantiation682, 677, 637  ⊢  
  : , : , :
304conjecture  ⊢  
 proveit.numbers.number_sets.natural_numbers.natural_pos_is_pos
305instantiation552, 672, 684, 610, 346, 612, 344, 525, 575  ⊢  
  : , : , : , : , : , :
306instantiation345, 610, 684, 612, 346, 525, 575  ⊢  
  : , : , : , :
307instantiation552, 672, 684, 610, 346, 612, 525, 575  ⊢  
  : , : , : , : , : , :
308instantiation350, 610, 684, 672, 612, 347, 525, 575, 348*  ⊢  
  : , : , : , : , : , :
309conjecture  ⊢  
 proveit.numbers.addition.subtraction.add_cancel_triple_32
310instantiation572  ⊢  
  :
311instantiation624  ⊢  
  : , :
312instantiation349, 672, 610, 612, 352, 575, 353  ⊢  
  : , : , : , : , : , : , :
313instantiation350, 610, 684, 672, 612, 351, 352, 353, 575, 354*  ⊢  
  : , : , : , : , : , :
314instantiation427, 355, 356,  ⊢  
  : , : , :
315instantiation601, 357, 358,  ⊢  
  : , : , :
316instantiation359, 679  ⊢  
  : , : , : , : , : , : , :
317generalization360  ⊢  
318conjecture  ⊢  
 proveit.core_expr_types.conditionals.satisfied_condition_reduction
319instantiation361, 679, 454, 390  ⊢  
  : , : , : , : , : , : , : , :
320modus ponens362, 363  ⊢  
321modus ponens364, 365  ⊢  
322instantiation624  ⊢  
  : , :
323conjecture  ⊢  
 proveit.numbers.multiplication.mult_nat_pos_closure_bin
324conjecture  ⊢  
 proveit.linear_algebra.addition.binary_closure
325conjecture  ⊢  
 proveit.physics.quantum.algebra.ket_zero_in_qubit_space
326instantiation453, 485, 390, 488  ⊢  
  : , : , : , :
327instantiation391, 679, 486  ⊢  
  : , : , : , : , : , :
328generalization366  ⊢  
329instantiation540, 644, 367  ⊢  
  : , :
330instantiation427, 466, 464  ⊢  
  : , : , :
331instantiation540, 644, 430  ⊢  
  : , :
332instantiation427, 470, 468  ⊢  
  : , : , :
333instantiation615, 368  ⊢  
  : , : , :
334instantiation586, 613, 369, 370, 371*  ⊢  
  : , :
335instantiation601, 372, 373  ⊢  
  : , : , :
336conjecture  ⊢  
 proveit.numbers.negation.int_neg_closure
337conjecture  ⊢  
 proveit.numbers.number_sets.integers.nonpos_int_is_int_nonpos
338instantiation374, 441, 625, 631, 375, 376*, 377*  ⊢  
  : , : , :
339conjecture  ⊢  
 proveit.numbers.negation.double_negation
340instantiation624  ⊢  
  : , :
341conjecture  ⊢  
 proveit.numbers.addition.subtraction.add_cancel_triple_12
342conjecture  ⊢  
 proveit.numbers.addition.elim_zero_left
343instantiation543, 378, 379,  ⊢  
  : , : , :
344conjecture  ⊢  
 proveit.numbers.number_sets.complex_numbers.zero_is_complex
345conjecture  ⊢  
 proveit.numbers.addition.elim_zero_any
346instantiation624  ⊢  
  : , :
347instantiation624  ⊢  
  : , :
348instantiation460, 380, 478*  ⊢  
  : , :
349conjecture  ⊢  
 proveit.numbers.addition.leftward_commutation
350conjecture  ⊢  
 proveit.numbers.addition.association
351instantiation624  ⊢  
  : , :
352instantiation682, 655, 381  ⊢  
  : , : , :
353instantiation682, 655, 382  ⊢  
  : , : , :
354instantiation601, 383, 384, 385*  ⊢  
  : , : , :
355instantiation615, 386,  ⊢  
  : , : , :
356instantiation387, 527, 491, 426,  ⊢  
  : , : , :
357instantiation460, 388,  ⊢  
  : , :
358instantiation389, 671, 622,  ⊢  
  : , :
359conjecture  ⊢  
 proveit.core_expr_types.lambda_maps.general_lambda_substitution
360instantiation617, 457, 390,  ⊢  
  : , :
361conjecture  ⊢  
 proveit.linear_algebra.scalar_multiplication.distribution_over_vec_sum_with_scalar_mult
362instantiation391, 679, 454  ⊢  
  : , : , : , : , : , :
363generalization428  ⊢  
364instantiation392, 672, 679, 610, 454, 612  ⊢  
  : , : , : , : , : , : , : , : , : , : , :
365generalization393  ⊢  
366instantiation453, 486, 457, 489,  ⊢  
  : , : , : , :
367instantiation394, 395, 396  ⊢  
  : , :
368instantiation601, 397, 398  ⊢  
  : , : , :
369instantiation579, 465, 469  ⊢  
  : , :
370instantiation399, 684, 400, 401, 402  ⊢  
  : , :
371instantiation601, 403, 404  ⊢  
  : , : , :
372instantiation615, 405  ⊢  
  : , : , :
373instantiation615, 406  ⊢  
  : , : , :
374conjecture  ⊢  
 proveit.numbers.addition.weak_bound_via_left_term_bound
375instantiation407, 671  ⊢  
  :
376instantiation492, 613, 408  ⊢  
  : , :
377instantiation409, 618, 410  ⊢  
  : , :
378instantiation579, 546, 411,  ⊢  
  : , :
379instantiation601, 412, 413,  ⊢  
  : , : , :
380instantiation609, 610, 684, 672, 612, 414, 613, 525, 420*  ⊢  
  : , : , : , : , : , :
381instantiation682, 668, 415  ⊢  
  : , : , :
382instantiation682, 668, 416  ⊢  
  : , : , :
383instantiation615, 417  ⊢  
  : , : , :
384instantiation460, 418  ⊢  
  : , :
385instantiation601, 419, 420  ⊢  
  : , : , :
386instantiation609, 421, 684, 610, 422, 423, 612, 644, 567, 580, 581, 566, 525,  ⊢  
  : , : , : , : , : , :
387conjecture  ⊢  
 proveit.numbers.exponentiation.product_of_complex_powers
388instantiation424, 425,  ⊢  
  : , : , :
389conjecture  ⊢  
 proveit.physics.quantum.algebra.prepend_num_ket_with_one_ket
390instantiation540, 490, 426  ⊢  
  : , :
391conjecture  ⊢  
 proveit.linear_algebra.addition.summation_closure
392conjecture  ⊢  
 proveit.linear_algebra.tensors.tensor_prod_distribution_over_summation_with_scalar_mult
393instantiation427, 428, 429,  ⊢  
  : , : , :
394conjecture  ⊢  
 proveit.numbers.addition.add_complex_closure_bin
395instantiation458, 608, 644, 587  ⊢  
  : , :
396instantiation590, 430  ⊢  
  :
397instantiation615, 550  ⊢  
  : , : , :
398instantiation601, 431, 432  ⊢  
  : , : , :
399conjecture  ⊢  
 proveit.numbers.multiplication.mult_not_eq_zero
400instantiation624  ⊢  
  : , :
401instantiation433, 465, 466  ⊢  
  :
402instantiation433, 469, 470  ⊢  
  :
403instantiation615, 434  ⊢  
  : , : , :
404instantiation601, 435, 436  ⊢  
  : , : , :
405instantiation601, 437, 438  ⊢  
  : , : , :
406instantiation601, 439, 440  ⊢  
  : , : , :
407conjecture  ⊢  
 proveit.numbers.number_sets.natural_numbers.natural_pos_lower_bound
408instantiation682, 655, 441  ⊢  
  : , : , :
409conjecture  ⊢  
 proveit.numbers.addition.subtraction.add_cancel_basic
410instantiation572  ⊢  
  :
411instantiation543, 442, 443,  ⊢  
  : , : , :
412instantiation574, 672, 547, 610, 444, 612, 546, 580, 505, 581,  ⊢  
  : , : , : , : , : , :
413instantiation574, 610, 684, 547, 612, 548, 444, 644, 567, 580, 505, 581,  ⊢  
  : , : , : , : , : , :
414instantiation624  ⊢  
  : , :
415instantiation682, 677, 445  ⊢  
  : , : , :
416instantiation682, 677, 446  ⊢  
  : , : , :
417instantiation460, 447  ⊢  
  : , :
418instantiation609, 610, 684, 672, 612, 448, 644, 575, 525  ⊢  
  : , : , : , : , : , :
419instantiation615, 449  ⊢  
  : , : , :
420instantiation522, 525  ⊢  
  :
421conjecture  ⊢  
 proveit.numbers.numerals.decimals.nat4
422instantiation450  ⊢  
  : , : , : , :
423instantiation624  ⊢  
  : , :
424theorem  ⊢  
 proveit.physics.quantum.algebra.num_ket_eq
425instantiation492, 525, 566,  ⊢  
  : , :
426instantiation543, 451, 452  ⊢  
  : , : , :
427theorem  ⊢  
 proveit.logic.equality.sub_left_side_into
428instantiation453, 454, 457, 455,  ⊢  
  : , : , : , :
429instantiation456, 457, 672, 610, 612, 485, 486, 488, 489,  ⊢  
  : , : , : , : , : , : , : , : , : , :
430instantiation458, 618, 644, 587  ⊢  
  : , :
431instantiation615, 459  ⊢  
  : , : , :
432instantiation460, 461  ⊢  
  : , :
433conjecture  ⊢  
 proveit.numbers.number_sets.complex_numbers.nonzero_complex_is_complex_nonzero
434instantiation462, 465, 469, 538, 466, 470, 518*, 521*  ⊢  
  : , : , :
435instantiation574, 672, 684, 610, 463, 612, 613, 519, 523  ⊢  
  : , : , : , : , : , :
436instantiation591, 610, 684, 612, 463, 519, 523  ⊢  
  : , : , : , :
437instantiation615, 464  ⊢  
  : , : , :
438instantiation586, 613, 465, 466, 467*  ⊢  
  : , :
439instantiation615, 468  ⊢  
  : , : , :
440instantiation586, 613, 469, 470, 471*  ⊢  
  : , :
441instantiation682, 668, 472  ⊢  
  : , : , :
442instantiation579, 473, 581,  ⊢  
  : , :
443instantiation574, 610, 684, 672, 612, 474, 580, 505, 581,  ⊢  
  : , : , : , : , : , :
444instantiation568  ⊢  
  : , : , :
445instantiation475, 678, 649  ⊢  
  : , :
446instantiation662, 649  ⊢  
  :
447instantiation476, 525  ⊢  
  :
448instantiation624  ⊢  
  : , :
449instantiation477, 613, 644, 478  ⊢  
  : , : , :
450conjecture  ⊢  
 proveit.numbers.numerals.decimals.tuple_len_4_typical_eq
451instantiation579, 546, 479  ⊢  
  : , :
452instantiation601, 480, 481  ⊢  
  : , : , :
453conjecture  ⊢  
 proveit.linear_algebra.scalar_multiplication.scalar_mult_closure
454instantiation482, 681, 484, 485, 486  ⊢  
  : , : , :
455instantiation483, 681, 484, 485, 486, 487, 488, 489,  ⊢  
  : , : , : , :
456conjecture  ⊢  
 proveit.linear_algebra.tensors.factor_scalar_from_tensor_prod
457instantiation540, 490, 491,  ⊢  
  : , :
458conjecture  ⊢  
 proveit.numbers.division.div_complex_closure
459instantiation492, 571, 627  ⊢  
  : , :
460theorem  ⊢  
 proveit.logic.equality.equals_reversal
461instantiation493, 644, 494, 495  ⊢  
  : , : , :
462conjecture  ⊢  
 proveit.numbers.exponentiation.real_power_of_product
463instantiation624  ⊢  
  : , :
464instantiation615, 496  ⊢  
  : , : , :
465instantiation497, 644  ⊢  
  :
466instantiation501, 654, 498  ⊢  
  : , :
467instantiation601, 499, 500  ⊢  
  : , : , :
468instantiation615, 570  ⊢  
  : , : , :
469instantiation540, 644, 571  ⊢  
  : , :
470instantiation501, 654, 502  ⊢  
  : , :
471instantiation601, 503, 504  ⊢  
  : , : , :
472instantiation682, 677, 634  ⊢  
  : , : , :
473instantiation579, 580, 505,  ⊢  
  : , :
474instantiation624  ⊢  
  : , :
475conjecture  ⊢  
 proveit.numbers.multiplication.mult_int_closure_bin
476conjecture  ⊢  
 proveit.numbers.negation.mult_neg_one_left
477conjecture  ⊢  
 proveit.numbers.addition.subtraction.subtract_from_add
478conjecture  ⊢  
 proveit.numbers.numerals.decimals.add_1_1
479instantiation543, 506, 507  ⊢  
  : , : , :
480instantiation574, 672, 547, 610, 508, 612, 546, 580, 581, 525  ⊢  
  : , : , : , : , : , :
481instantiation574, 610, 684, 547, 612, 548, 508, 644, 567, 580, 581, 525  ⊢  
  : , : , : , : , : , :
482conjecture  ⊢  
 proveit.linear_algebra.tensors.tensor_prod_of_vec_spaces_is_vec_space
483conjecture  ⊢  
 proveit.linear_algebra.tensors.tensor_prod_is_in_tensor_prod_space
484instantiation624  ⊢  
  : , :
485instantiation509, 681  ⊢  
  :
486instantiation509, 510  ⊢  
  :
487instantiation624  ⊢  
  : , :
488conjecture  ⊢  
 proveit.physics.quantum.algebra.ket_one_in_qubit_space
489instantiation511, 671, 622,  ⊢  
  : , :
490instantiation682, 655, 512  ⊢  
  : , : , :
491instantiation543, 513, 514,  ⊢  
  : , : , :
492conjecture  ⊢  
 proveit.numbers.addition.commutation
493conjecture  ⊢  
 proveit.numbers.exponentiation.product_of_pos_powers
494instantiation682, 515, 665  ⊢  
  : , : , :
495instantiation682, 515, 619  ⊢  
  : , : , :
496instantiation601, 516, 517  ⊢  
  : , : , :
497conjecture  ⊢  
 proveit.numbers.exponentiation.sqrt_complex_closure
498instantiation682, 520, 665  ⊢  
  : , : , :
499instantiation615, 518  ⊢  
  : , : , :
500instantiation522, 519  ⊢  
  :
501conjecture  ⊢  
 proveit.numbers.exponentiation.exp_rational_non_zero__not_zero
502instantiation682, 520, 619  ⊢  
  : , : , :
503instantiation615, 521  ⊢  
  : , : , :
504instantiation522, 523  ⊢  
  :
505instantiation540, 644, 524,  ⊢  
  : , :
506instantiation579, 564, 525  ⊢  
  : , :
507instantiation574, 610, 684, 672, 612, 565, 580, 581, 525  ⊢  
  : , : , : , : , : , :
508instantiation568  ⊢  
  : , : , :
509conjecture  ⊢  
 proveit.linear_algebra.complex_vec_set_is_vec_space
510instantiation526, 684, 661  ⊢  
  : , :
511conjecture  ⊢  
 proveit.physics.quantum.algebra.num_ket_in_register_space
512instantiation682, 596, 527  ⊢  
  : , : , :
513instantiation579, 546, 528,  ⊢  
  : , :
514instantiation601, 529, 530,  ⊢  
  : , : , :
515conjecture  ⊢  
 proveit.numbers.number_sets.real_numbers.rational_pos_within_real_pos
516instantiation601, 531, 532  ⊢  
  : , : , :
517instantiation601, 533, 534  ⊢  
  : , : , :
518instantiation537, 644, 640, 538, 587, 535*  ⊢  
  : , : , :
519instantiation540, 644, 536  ⊢  
  : , :
520conjecture  ⊢  
 proveit.numbers.number_sets.rational_numbers.rational_pos_within_rational_nonzero
521instantiation537, 644, 589, 538, 587, 539*  ⊢  
  : , : , :
522conjecture  ⊢  
 proveit.numbers.multiplication.elim_one_left
523instantiation540, 644, 554  ⊢  
  : , :
524instantiation590, 541,  ⊢  
  :
525instantiation682, 655, 542  ⊢  
  : , : , :
526conjecture  ⊢  
 proveit.numbers.exponentiation.exp_natpos_closure
527conjecture  ⊢  
 proveit.numbers.number_sets.real_numbers.e_is_real_pos
528instantiation543, 544, 545,  ⊢  
  : , : , :
529instantiation574, 672, 547, 610, 549, 612, 546, 580, 581, 566,  ⊢  
  : , : , : , : , : , :
530instantiation574, 610, 684, 547, 612, 548, 549, 644, 567, 580, 581, 566,  ⊢  
  : , : , : , : , : , :
531instantiation615, 550  ⊢  
  : , : , :
532instantiation615, 551  ⊢  
  : , : , :
533instantiation552, 610, 684, 672, 612, 553, 571, 627, 554  ⊢  
  : , : , : , : , : , :
534instantiation555, 571, 627, 556  ⊢  
  : , : , :
535instantiation557, 627, 613, 614*  ⊢  
  : , :
536instantiation682, 655, 558  ⊢  
  : , : , :
537conjecture  ⊢  
 proveit.numbers.exponentiation.real_power_of_real_power
538instantiation682, 668, 559  ⊢  
  : , : , :
539instantiation601, 560, 561  ⊢  
  : , : , :
540conjecture  ⊢  
 proveit.numbers.exponentiation.exp_complex_closure
541instantiation682, 655, 562,  ⊢  
  : , : , :
542instantiation682, 668, 563  ⊢  
  : , : , :
543theorem  ⊢  
 proveit.logic.equality.sub_right_side_into
544instantiation579, 564, 566,  ⊢  
  : , :
545instantiation574, 610, 684, 672, 612, 565, 580, 581, 566,  ⊢  
  : , : , : , : , : , :
546instantiation579, 644, 567  ⊢  
  : , :
547conjecture  ⊢  
 proveit.numbers.numerals.decimals.nat3
548instantiation624  ⊢  
  : , :
549instantiation568  ⊢  
  : , : , :
550instantiation586, 608, 644, 587, 569*  ⊢  
  : , :
551instantiation615, 570  ⊢  
  : , : , :
552conjecture  ⊢  
 proveit.numbers.addition.disassociation
553instantiation624  ⊢  
  : , :
554instantiation590, 571  ⊢  
  :
555conjecture  ⊢  
 proveit.numbers.addition.subtraction.add_cancel_triple_13
556instantiation572  ⊢  
  :
557conjecture  ⊢  
 proveit.numbers.negation.pos_times_neg
558instantiation573, 640  ⊢  
  :
559instantiation682, 677, 650  ⊢  
  : , : , :
560instantiation574, 610, 684, 672, 612, 592, 627, 618, 575  ⊢  
  : , : , : , : , : , :
561instantiation576, 684, 610, 592, 612, 627, 618, 613, 577*  ⊢  
  : , : , : , : , :
562instantiation682, 668, 578,  ⊢  
  : , : , :
563instantiation682, 677, 649  ⊢  
  : , : , :
564instantiation579, 580, 581  ⊢  
  : , :
565instantiation624  ⊢  
  : , :
566instantiation682, 655, 582,  ⊢  
  : , : , :
567instantiation682, 655, 583  ⊢  
  : , : , :
568conjecture  ⊢  
 proveit.numbers.numerals.decimals.tuple_len_3_typical_eq
569instantiation601, 584, 585  ⊢  
  : , : , :
570instantiation586, 618, 644, 587, 588*  ⊢  
  : , :
571instantiation682, 655, 589  ⊢  
  : , : , :
572axiom  ⊢  
 proveit.logic.equality.equals_reflexivity
573conjecture  ⊢  
 proveit.numbers.negation.real_closure
574conjecture  ⊢  
 proveit.numbers.multiplication.disassociation
575instantiation590, 613  ⊢  
  :
576conjecture  ⊢  
 proveit.numbers.multiplication.mult_neg_any
577instantiation591, 684, 610, 592, 612, 627, 618  ⊢  
  : , : , : , :
578instantiation682, 677, 593,  ⊢  
  : , : , :
579conjecture  ⊢  
 proveit.numbers.multiplication.mult_complex_closure_bin
580conjecture  ⊢  
 proveit.numbers.number_sets.complex_numbers.i_is_complex
581instantiation682, 655, 594  ⊢  
  : , : , :
582instantiation682, 668, 595,  ⊢  
  : , : , :
583instantiation682, 596, 597  ⊢  
  : , : , :
584instantiation615, 616  ⊢  
  : , : , :
585instantiation601, 598, 599  ⊢  
  : , : , :
586conjecture  ⊢  
 proveit.numbers.division.div_as_mult
587instantiation600, 681  ⊢  
  :
588instantiation601, 602, 603  ⊢  
  : , : , :
589instantiation682, 668, 604  ⊢  
  : , : , :
590conjecture  ⊢  
 proveit.numbers.negation.complex_closure
591conjecture  ⊢  
 proveit.numbers.multiplication.elim_one_any
592instantiation624  ⊢  
  : , :
593instantiation682, 605, 606,  ⊢  
  : , : , :
594conjecture  ⊢  
 proveit.physics.quantum.QPE._phase_is_real
595instantiation682, 677, 607,  ⊢  
  : , : , :
596conjecture  ⊢  
 proveit.numbers.number_sets.real_numbers.real_pos_within_real
597conjecture  ⊢  
 proveit.numbers.number_sets.real_numbers.pi_is_real_pos
598instantiation617, 608, 627  ⊢  
  : , :
599instantiation609, 672, 684, 610, 611, 612, 627, 618, 613, 614*  ⊢  
  : , : , : , : , : , :
600conjecture  ⊢  
 proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos
601axiom  ⊢  
 proveit.logic.equality.equals_transitivity
602instantiation615, 616  ⊢  
  : , : , :
603instantiation617, 618, 627  ⊢  
  : , :
604instantiation682, 664, 619  ⊢  
  : , : , :
605instantiation635, 620, 636  ⊢  
  : , :
606assumption  ⊢  
607instantiation682, 621, 622,  ⊢  
  : , : , :
608instantiation682, 655, 623  ⊢  
  : , : , :
609conjecture  ⊢  
 proveit.numbers.multiplication.distribute_through_sum
610axiom  ⊢  
 proveit.numbers.number_sets.natural_numbers.zero_in_nats
611instantiation624  ⊢  
  : , :
612conjecture  ⊢  
 proveit.core_expr_types.tuples.tuple_len_0_typical_eq
613instantiation682, 655, 625  ⊢  
  : , : , :
614instantiation626, 627  ⊢  
  :
615axiom  ⊢  
 proveit.logic.equality.substitution
616instantiation628, 629, 679, 630*  ⊢  
  : , :
617conjecture  ⊢  
 proveit.numbers.multiplication.commutation
618instantiation682, 655, 631  ⊢  
  : , : , :
619instantiation632, 665, 633  ⊢  
  : , :
620instantiation648, 634, 663  ⊢  
  : , :
621instantiation635, 636, 637  ⊢  
  : , :
622assumption  ⊢  
623instantiation645, 646, 638  ⊢  
  : , : , :
624conjecture  ⊢  
 proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
625instantiation682, 668, 639  ⊢  
  : , : , :
626conjecture  ⊢  
 proveit.numbers.multiplication.elim_one_right
627instantiation682, 655, 640  ⊢  
  : , : , :
628conjecture  ⊢  
 proveit.numbers.exponentiation.neg_power_as_div
629instantiation682, 641, 642  ⊢  
  : , : , :
630instantiation643, 644  ⊢  
  :
631instantiation645, 646, 671  ⊢  
  : , : , :
632conjecture  ⊢  
 proveit.numbers.multiplication.mult_rational_pos_closure_bin
633instantiation682, 680, 671  ⊢  
  : , : , :
634instantiation662, 647  ⊢  
  :
635conjecture  ⊢  
 proveit.numbers.number_sets.integers.int_interval_within_int
636conjecture  ⊢  
 proveit.numbers.number_sets.integers.zero_is_int
637instantiation648, 649, 650  ⊢  
  : , :
638instantiation651, 671, 679  ⊢  
  : , :
639instantiation682, 677, 663  ⊢  
  : , : , :
640instantiation682, 668, 652  ⊢  
  : , : , :
641conjecture  ⊢  
 proveit.numbers.number_sets.complex_numbers.real_nonzero_within_complex_nonzero
642instantiation682, 653, 654  ⊢  
  : , : , :
643conjecture  ⊢  
 proveit.numbers.exponentiation.complex_x_to_first_power_is_x
644instantiation682, 655, 656  ⊢  
  : , : , :
645theorem  ⊢  
 proveit.logic.sets.inclusion.unfold_subset_eq
646instantiation657, 658  ⊢  
  : , :
647instantiation682, 659, 671  ⊢  
  : , : , :
648conjecture  ⊢  
 proveit.numbers.addition.add_int_closure_bin
649instantiation660, 678, 661  ⊢  
  : , :
650instantiation662, 663  ⊢  
  :
651conjecture  ⊢  
 proveit.numbers.addition.add_nat_pos_closure_bin
652instantiation682, 664, 665  ⊢  
  : , : , :
653conjecture  ⊢  
 proveit.numbers.number_sets.real_numbers.rational_nonzero_within_real_nonzero
654instantiation682, 666, 667  ⊢  
  : , : , :
655conjecture  ⊢  
 proveit.numbers.number_sets.complex_numbers.real_within_complex
656instantiation682, 668, 669  ⊢  
  : , : , :
657theorem  ⊢  
 proveit.logic.sets.inclusion.relax_proper_subset
658conjecture  ⊢  
 proveit.numbers.number_sets.real_numbers.nat_pos_within_real
659conjecture  ⊢  
 proveit.numbers.number_sets.integers.nat_pos_within_int
660conjecture  ⊢  
 proveit.numbers.exponentiation.exp_int_closure
661instantiation682, 670, 671  ⊢  
  : , : , :
662conjecture  ⊢  
 proveit.numbers.negation.int_closure
663instantiation682, 683, 672  ⊢  
  : , : , :
664conjecture  ⊢  
 proveit.numbers.number_sets.rational_numbers.rational_pos_within_rational
665instantiation673, 674, 675  ⊢  
  : , :
666conjecture  ⊢  
 proveit.numbers.number_sets.rational_numbers.nonzero_int_within_rational_nonzero
667instantiation682, 676, 681  ⊢  
  : , : , :
668conjecture  ⊢  
 proveit.numbers.number_sets.real_numbers.rational_within_real
669instantiation682, 677, 678  ⊢  
  : , : , :
670conjecture  ⊢  
 proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat
671assumption  ⊢  
672theorem  ⊢  
 proveit.numbers.numerals.decimals.nat1
673conjecture  ⊢  
 proveit.numbers.division.div_rational_pos_closure
674instantiation682, 680, 679  ⊢  
  : , : , :
675instantiation682, 680, 681  ⊢  
  : , : , :
676conjecture  ⊢  
 proveit.numbers.number_sets.integers.nat_pos_within_nonzero_int
677conjecture  ⊢  
 proveit.numbers.number_sets.rational_numbers.int_within_rational
678instantiation682, 683, 684  ⊢  
  : , : , :
679conjecture  ⊢  
 proveit.numbers.numerals.decimals.posnat1
680conjecture  ⊢  
 proveit.numbers.number_sets.rational_numbers.nat_pos_within_rational_pos
681conjecture  ⊢  
 proveit.numbers.numerals.decimals.posnat2
682theorem  ⊢  
 proveit.logic.sets.inclusion.superset_membership_from_proper_subset
683conjecture  ⊢  
 proveit.numbers.number_sets.integers.nat_within_int
684theorem  ⊢  
 proveit.numbers.numerals.decimals.nat2
*equality replacement requirements